ePMC

java -Xms10240m -Xmx10240m -jar ./root/epmc-standard.jar check --model-input-files cluster.prism --model-input-type prism --property-input-files cluster.props --property-input-names qos1 --translate-messages false --value-floating-point-output-native true --graphsolver-iterative-stop-criterion relative --graphsolver-iterative-tolerance 1e-6 --const N=128,T=2000,t=20

assertions-disabled
start-parsing
done-parsing
model-checking
analysing-property qos1
start-building-explorer
start-building-initial-states-explorer
done-building-initial-states-explorer
done-building-explorer
build-model-start
build-model-states-explored 28267 28267
build-model-states-explored 66760 38493
build-model-states-explored 106757 39997
build-model-states-explored 153208 46450
build-model-states-explored 207060 53852
build-model-states-explored 258168 51108
build-model-states-explored 304305 46137
build-model-states-explored 358313 54009
build-model-states-explored 410631 52317
build-model-states-explored 460842 50212
build-model-states-explored 516169 55326
build-model-states-explored 554159 37990
build-model-done 597012 12
iterating-progress-bounded 469 83030 0.005648560761170662 1
iterating-progress-bounded 981 83030 0.011815006624111767 2
iterating-progress-bounded 1493 83030 0.017981452487052872 3
iterating-progress-bounded 2006 83030 0.024159942189570034 4
iterating-progress-bounded 2520 83030 0.030350475731663253 5
iterating-progress-bounded 3033 83030 0.03652896543418042 6
iterating-progress-bounded 3546 83030 0.04270745513669758 7
iterating-progress-bounded 4059 83030 0.04888594483921474 8
iterating-progress-bounded 4573 83030 0.05507647838130796 9
iterating-progress-bounded 5087 83030 0.06126701192340118 10
iterating-progress-bounded 5601 83030 0.0674575454654944 11
iterating-progress-bounded 6115 83030 0.07364807900758762 12
iterating-progress-bounded 6629 83030 0.07983861254968083 13
iterating-progress-bounded 7143 83030 0.08602914609177406 14
iterating-progress-bounded 7657 83030 0.09221967963386728 15
iterating-progress-bounded 8171 83030 0.09841021317596049 16
iterating-progress-bounded 8685 83030 0.10460074671805372 17
iterating-progress-bounded 9198 83030 0.11077923642057087 18
iterating-progress-bounded 9712 83030 0.1169697699626641 19
iterating-progress-bounded 10226 83030 0.12316030350475732 20
iterating-progress-bounded 10740 83030 0.12935083704685055 21
iterating-progress-bounded 11254 83030 0.13554137058894375 22
iterating-progress-bounded 11763 83030 0.14167168493315668 23
iterating-progress-bounded 12277 83030 0.1478622184752499 24
iterating-progress-bounded 12791 83030 0.15405275201734314 25
iterating-progress-bounded 13305 83030 0.16024328555943634 26
iterating-progress-bounded 13819 83030 0.16643381910152957 27
iterating-progress-bounded 14332 83030 0.17261230880404674 28
iterating-progress-bounded 14846 83030 0.17880284234613994 29
iterating-progress-bounded 15360 83030 0.18499337588823317 30
iterating-progress-bounded 15874 83030 0.1911839094303264 31
iterating-progress-bounded 16388 83030 0.1973744429724196 32
iterating-progress-bounded 16902 83030 0.20356497651451283 33
iterating-progress-bounded 17416 83030 0.20975551005660606 34
iterating-progress-bounded 17930 83030 0.21594604359869926 35
iterating-progress-bounded 18444 83030 0.2221365771407925 36
iterating-progress-bounded 18958 83030 0.2283271106828857 37
iterating-progress-bounded 19472 83030 0.23451764422497892 38
iterating-progress-bounded 19986 83030 0.24070817776707215 39
iterating-progress-bounded 20500 83030 0.24689871130916535 40
iterating-progress-bounded 21014 83030 0.25308924485125855 41
iterating-progress-bounded 21528 83030 0.2592797783933518 42
iterating-progress-bounded 22041 83030 0.265458268095869 43
iterating-progress-bounded 22555 83030 0.2716488016379622 44
iterating-progress-bounded 23070 83030 0.2778513790196315 45
iterating-progress-bounded 23583 83030 0.28402986872214864 46
iterating-progress-bounded 24097 83030 0.29022040226424184 47
iterating-progress-bounded 24610 83030 0.296398891966759 48
iterating-progress-bounded 25123 83030 0.30257738166927617 49
iterating-progress-bounded 25636 83030 0.30875587137179333 50
iterating-progress-bounded 26150 83030 0.31494640491388654 51
iterating-progress-bounded 26664 83030 0.3211369384559798 52
iterating-progress-bounded 27172 83030 0.32725520896061666 53
iterating-progress-bounded 27686 83030 0.33344574250270986 54
iterating-progress-bounded 28200 83030 0.33963627604480306 55
iterating-progress-bounded 28714 83030 0.3458268095868963 56
iterating-progress-bounded 29228 83030 0.3520173431289895 57
iterating-progress-bounded 29742 83030 0.3582078766710827 58
iterating-progress-bounded 30256 83030 0.364398410213176 59
iterating-progress-bounded 30770 83030 0.3705889437552692 60
iterating-progress-bounded 31284 83030 0.3767794772973624 61
iterating-progress-bounded 31789 83030 0.3828616162832711 62
iterating-progress-bounded 32303 83030 0.38905214982536435 63
iterating-progress-bounded 32817 83030 0.39524268336745755 64
iterating-progress-bounded 33331 83030 0.40143321690955075 65
iterating-progress-bounded 33845 83030 0.407623750451644 66
iterating-progress-bounded 34359 83030 0.4138142839937372 67
iterating-progress-bounded 34873 83030 0.4200048175358304 68
iterating-progress-bounded 35384 83030 0.42615921955919545 69
iterating-progress-bounded 35898 83030 0.4323497531012887 70
iterating-progress-bounded 36412 83030 0.4385402866433819 71
iterating-progress-bounded 36926 83030 0.4447308201854751 72
iterating-progress-bounded 37440 83030 0.45092135372756836 73
iterating-progress-bounded 37955 83030 0.4571239311092376 74
iterating-progress-bounded 38468 83030 0.46330242081175477 75
iterating-progress-bounded 38983 83030 0.46950499819342406 76
iterating-progress-bounded 39497 83030 0.47569553173551726 77
iterating-progress-bounded 40006 83030 0.4818258460797302 78
iterating-progress-bounded 40519 83030 0.4880043357822474 79
iterating-progress-bounded 41030 83030 0.4941587378056124 80
iterating-progress-bounded 41544 83030 0.5003492713477057 81
iterating-progress-bounded 42058 83030 0.5065398048897989 82
iterating-progress-bounded 42568 83030 0.5126821630735878 83
iterating-progress-bounded 43075 83030 0.5187883897386487 84
iterating-progress-bounded 43589 83030 0.5249789232807419 85
iterating-progress-bounded 44099 83030 0.5311212814645309 86
iterating-progress-bounded 44612 83030 0.5372997711670481 87
iterating-progress-bounded 45126 83030 0.5434903047091413 88
iterating-progress-bounded 45640 83030 0.5496808382512345 89
iterating-progress-bounded 46154 83030 0.5558713717933277 90
iterating-progress-bounded 46668 83030 0.5620619053354209 91
iterating-progress-bounded 47182 83030 0.5682524388775142 92
iterating-progress-bounded 47696 83030 0.5744429724196074 93
iterating-progress-bounded 48210 83030 0.5806335059617006 94
iterating-progress-bounded 48724 83030 0.5868240395037938 95
iterating-progress-bounded 49238 83030 0.593014573045887 96
iterating-progress-bounded 49752 83030 0.5992051065879802 97
iterating-progress-bounded 50266 83030 0.6053956401300735 98
iterating-progress-bounded 50780 83030 0.6115861736721667 99
iterating-progress-bounded 51290 83030 0.6177285318559557 100
iterating-progress-bounded 51804 83030 0.6239190653980489 101
iterating-progress-bounded 52314 83030 0.6300614235818379 102
iterating-progress-bounded 52828 83030 0.6362519571239311 103
iterating-progress-bounded 53342 83030 0.6424424906660243 104
iterating-progress-bounded 53856 83030 0.6486330242081175 105
iterating-progress-bounded 54370 83030 0.6548235577502107 106
iterating-progress-bounded 54884 83030 0.661014091292304 107
iterating-progress-bounded 55398 83030 0.6672046248343972 108
iterating-progress-bounded 55912 83030 0.6733951583764904 109
iterating-progress-bounded 56422 83030 0.6795375165602794 110
iterating-progress-bounded 56936 83030 0.6857280501023726 111
iterating-progress-bounded 57449 83030 0.6919065398048898 112
iterating-progress-bounded 57960 83030 0.6980609418282548 113
iterating-progress-bounded 58474 83030 0.704251475370348 114
iterating-progress-bounded 58987 83030 0.7104299650728653 115
iterating-progress-bounded 59497 83030 0.7165723232566542 116
iterating-progress-bounded 60011 83030 0.7227628567987474 117
iterating-progress-bounded 60525 83030 0.7289533903408406 118
iterating-progress-bounded 61039 83030 0.7351439238829339 119
iterating-progress-bounded 61553 83030 0.7413344574250271 120
iterating-progress-bounded 62067 83030 0.7475249909671203 121
iterating-progress-bounded 62580 83030 0.7537034806696374 122
iterating-progress-bounded 63093 83030 0.7598819703721547 123
iterating-progress-bounded 63608 83030 0.766084547753824 124
iterating-progress-bounded 64121 83030 0.7722630374563411 125
iterating-progress-bounded 64635 83030 0.7784535709984343 126
iterating-progress-bounded 65149 83030 0.7846441045405275 127
iterating-progress-bounded 65662 83030 0.7908225942430447 128
iterating-progress-bounded 66176 83030 0.7970131277851379 129
iterating-progress-bounded 66690 83030 0.8032036613272311 130
iterating-progress-bounded 67204 83030 0.8093941948693243 131
iterating-progress-bounded 67717 83030 0.8155726845718415 132
iterating-progress-bounded 68231 83030 0.8217632181139347 133
iterating-progress-bounded 68745 83030 0.8279537516560279 134
iterating-progress-bounded 69259 83030 0.8341442851981211 135
iterating-progress-bounded 69772 83030 0.8403227749006383 136
iterating-progress-bounded 70286 83030 0.8465133084427315 137
iterating-progress-bounded 70800 83030 0.8527038419848247 138
iterating-progress-bounded 71313 83030 0.858882331687342 139
iterating-progress-bounded 71827 83030 0.8650728652294352 140
iterating-progress-bounded 72341 83030 0.8712633987715284 141
iterating-progress-bounded 72855 83030 0.8774539323136216 142
iterating-progress-bounded 73363 83030 0.8835722028182584 143
iterating-progress-bounded 73877 83030 0.8897627363603516 144
iterating-progress-bounded 74391 83030 0.895953269902445 145
iterating-progress-bounded 74905 83030 0.9021438034445382 146
iterating-progress-bounded 75418 83030 0.9083222931470553 147
iterating-progress-bounded 75932 83030 0.9145128266891485 148
iterating-progress-bounded 76446 83030 0.9207033602312418 149
iterating-progress-bounded 76960 83030 0.926893893773335 150
iterating-progress-bounded 77473 83030 0.9330723834758521 151
iterating-progress-bounded 77987 83030 0.9392629170179453 152
iterating-progress-bounded 78501 83030 0.9454534505600385 153
iterating-progress-bounded 79015 83030 0.9516439841021318 154
iterating-progress-bounded 79528 83030 0.9578224738046489 155
iterating-progress-bounded 80042 83030 0.9640130073467421 156
iterating-progress-bounded 80556 83030 0.9702035408888353 157
iterating-progress-bounded 81065 83030 0.9763338552330483 158
iterating-progress-bounded 81579 83030 0.9825243887751415 159
iterating-progress-bounded 82092 83030 0.9887028784776587 160
iterating-progress-bounded 82606 83030 0.9948934120197519 161
model-checking-done 177
command-check-result-is 0.001072402538813384 qos1